abstract sig User{}           // User is superclass of Customer and Employee

sig Customer extends User {
browse: some gPackage,
modify:lone pPackage,
ID:one Int
}{ID>0}

fact UniqId{                        // no shared ID
all e1,e2: Employee|e1!=e2 implies e1.ID!=e2.ID
all c1,c2:Customer|c1!=c2 implies c1.ID!=c2.ID
all e:Employee |all c:Customer|e.ID!=c.ID
}

sig Employee extends User{       // Employee creates some product and package
cProduct:some Product,
cPackage:set gPackage,
ID:one Int
}{#Employee >1
ID>0}

abstract sig Product {}            // Product is the superclass of Hotel,Flight and Excursion

sig Hotel extends Product{}

sig Flight extends Product{}

sig Excursion extends Product{}

sig gPackage{                         // general Package contains at least one Flight and Hotel and some 
fContent:some Flight,              //Excursion as its content 
hContent:some Hotel,
exContent:set Excursion
}

fact distinctPackage{              //Every general Package should have their distinct set of Products
all g1,g2: gPackage|g1!=g2 implies g1.(fContent+hContent)!=g2.(fContent+hContent)
}



fact packageFunctional{         //all Personalized Package should be personalized by a Customer
all p:pPackage|all c:Customer|p in c.modify
}

fact oneProductCreator{         // Each product should have been created by only one Employee
all p:Product | one e:Employee| p in e.cProduct
}

fact onePackageCreator{        //As above but for general Package
all p:gPackage|one e:Employee|p in e.cPackage
}



sig pPackage{
origin: one gPackage}

fact packageOrigin{               //The Origin of a Customer's pPackage should be one of the gPackage that
all c:Customer |c.modify.origin in c.browse}  // this customer browsed

sig cFriend{                         // Each friend relate to one Customer and he can either join his friend's
relate:one Customer,          //pPackage or not.
join:lone pPackage
}

fact joinFriendPackage{     //The package that a friend joined should be the one of his/her friend
all f:cFriend|f.join=f.relate.modify
}

pred show{
}

run show for 3 
